x:. if x then tt else inr (x.)  fi   Dec(x) 

latex

Definitions	False, t  T, Ax, x.A(x), P  Q, inr x , P  Q, A, , Dec(P), #$n, , x:A. B(x), x:AB(x), inl x , tt, True, Void, , b, b, s = t, , x:A  B(x), P & Q, P  Q, Unit, left + right
Lemmas	eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bnot wf, not wf, assert wf, bool wf, btrue wf, member wf, false wf